T:Type, L:(T List).
no_repeats(T;L)
 (A:Type, f:({x:T| (x  L)} A). Inj({x:T| (x  L)} ;A;f)  no_repeats(A;map(f;L))) 

latex

Definitions	no_repeats(T;l), P  Q, (x  l), {x:A| B(x)} , Inj(A;B;f), x:AB(x), x:A. B(x), Type, type List, t  T, A, s = t, hd(l), i <z j, i z j, l[i], P & Q, i  j < k, A  B, a < b, x:A  B(x), {i..j}, #$n, ||as||, n+m, Void, False, , , f(a), {T}, P  Q, P  Q, P  Q, S  T, [car / cdr], x. t(x), suptype(S; T), mapl(f;l), A c B, , i  j , x:A. B(x), s ~ t, SQType(T)
Lemmas	member-mapl, le wf, non neg length, nat wf, length wf1, select wf, no repeats cons, mapl wf, subtype rel function, subtype rel set, l member wf, cons member, select member, no repeats nil